ds:x:Id fp Type, da:k:Knd fp Type, A, B:ecl-trans-tuple{i:l}(ds;da), m:,
L:event-info(ds;da) List, z:event-info(ds;da).
let Ta,ksa,ia,ga,ha,aa,ea = A in 
let Tb,ksb,ib,gb,hb,ab,eb = B in 
Ta = Tb  Type
& ksa = ksb  Knd List & ia = ib  Ta
& aa = ab  (k:{k:Knd| (k  ksa) }State(ds)Valtype(da;k)Ta)
& & (L':event-info(ds;da) List, k:{k:Knd| (k  ksa) }, s:State(ds), v:Valtype(da;k).
& & (L' @ [<k,s,v>]  L  gb(k,s,v,ecl-trans-state(A;L')) = ga(k,s,v,ecl-trans-state(A;L'))  Ta)
 ecl-trans-act(ds;da;A)(m,L @ [z])
 ecl-trans-act(ds;da;B)(m,L @ [z]) 

latex

Definitions

t  T, x:A. B(x), P  Q, False, A, AB, , , , Valtype(da;k), State(ds), (x  l), ecl-trans-type(A), ecl-trans-tuple{i:l}(ds;da), S  T, ecl-trans-state(v;L), Top, KindDeq, x. t(x), f(x)?z, event-info(ds;da), b, Prop, A & B, as @ bs, P & Q, x:A. B(x), True, T, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), let x,y,z = a in t(x;y;z), ecl-trans-a(v), ecl-trans-ks(v), ecl-trans-act(ds;da;A), {T}, SQType(T), P  Q, ij, ||as||, S  T, l1  l2, a:A fp B(a), Id, Knd, b, deq-member(eq;x;L), Unit, if b t else f fi, list_accum(x,a.f(x;a);y;l), x,y. t(x;y), ecl-trans-state-from(v;z;L), ecl-trans-init(v)

Lemmas

append-cancellation-right, list accum wf, list accum functionality, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-deq-member, deq-member wf, bnot wf, not wf, Id wf, fpf wf, ecl-trans-tuple wf, iseg wf, le wf, length wf1, non neg length, cons one one, Knd sq, ecl-trans-act wf, squash wf, true wf, append wf, event-info wf, assert wf, fpf-cap wf, Kind-deq wf, top wf, ecl-trans-state wf, nat wf, l member wf, Knd wf, decl-state wf, ma-valtype wf, bool wf, nat plus wf, subtype rel self